COMMENT ⊗   VALID 00002 PAGES
C REC  PAGE   DESCRIPTION
C00001 00001
C00002 00002	(wipe-out) 51s				***bug?***
C00018 ENDMK
C⊗;
(wipe-out) ;51s				***bug?***
(proof foo)

1. (DEFINE A
     |∀AB FLIES.A(AB,FLIES)≡
                (∀X.¬AB(ASPECT1(X))⊃¬FLIES(X))∧(∀X.BIRD(X)⊃AB(ASPECT1(X)))∧
                (∀X.BIRD(X)∧¬AB(ASPECT2(X))⊃FLIES(X))∧
                (∀X.OSTRICH(X)⊃AB(ASPECT2(X)))∧
                (∀X.OSTRICH(X)∧¬AB(ASPECT3(X))⊃¬FLIES(X))| NIL)

2. (AXIOM
     |(∀X Y.¬ASPECT1(X)=ASPECT2(Y))∧(∀X Y.¬ASPECT1(X)=ASPECT3(Y))∧
      (∀X Y.¬ASPECT2(X)=ASPECT3(Y))∧(∀X Y.ASPECT1(X)=ASPECT1(Y)≡X=Y)∧
      (∀X Y.ASPECT2(X)=ASPECT2(Y)≡X=Y)∧(∀X Y.ASPECT3(X)=ASPECT3(Y)≡X=Y)|)
(label simpinfo)
(label unequal)

3. (DEFINE A1
     |∀AB FLIES.A1(AB,FLIES)≡
                A(AB,FLIES)∧
                (∀AB1 FLIES1.A(AB1,FLIES1)∧(∀Z.AB1(Z)⊃AB(Z))⊃(∀Z.AB(Z)≡AB1(Z)))|
     NIL)

4. (ASSUME |A1(AB,FLIES)|)
;deps: (4)

5. (DEFINE FLIES2 |∀X.FLIES2(X)≡BIRD(X)∧¬OSTRICH(X)| NIL)

6. (DEFINE AB2
     |∀Z.AB2(Z)≡(∃X.BIRD(X)∧Z=ASPECT1(X))∨(∃X.OSTRICH(X)∧Z=ASPECT2(X))| )

7. (RW 4 (USE 3 MODE: EXACT))
;A(AB,FLIES)∧(∀AB1 FLIES1.A(AB1,FLIES1)∧(∀Z.AB1(Z)⊃AB(Z))⊃(∀Z.AB(Z)≡AB1(Z)))
;deps: (4)

8. (TRW |A(AB,FLIES)| (USE 7))
;A(AB,FLIES)
;deps: (4)

9. (TRW |∀AB1 FLIES1.A(AB1,FLIES1)∧(∀Z.AB1(Z)⊃AB(Z))⊃(∀Z.AB(Z)≡AB1(Z))| 
	(USE 7))
;∀AB1 FLIES1.A(AB1,FLIES1)∧(∀Z.AB1(Z)⊃AB(Z))⊃(∀Z.AB(Z)≡AB1(Z))
;deps: (4)

10. (RW 8 (USE 1 MODE: EXACT))
;(∀X.¬AB(ASPECT1(X))⊃¬FLIES(X))∧(∀X.BIRD(X)⊃AB(ASPECT1(X)))∧
;(∀X.BIRD(X)∧¬AB(ASPECT2(X))⊃FLIES(X))∧(∀X.OSTRICH(X)⊃AB(ASPECT2(X)))∧
;(∀X.OSTRICH(X)∧¬AB(ASPECT3(X))⊃¬FLIES(X))
;deps: (4)

11. (ASSUME |AB2(Z)|)
;deps: (11)

12. (RW 11 (OPEN AB2))
;(∃X.BIRD(X)∧Z=ASPECT1(X))∨(∃X.OSTRICH(X)∧Z=ASPECT2(X))
;deps: (11)

13. (DERIVE |AB(Z)| (12 10) NIL)
;AB(Z)
;deps: (4 11)

14. (CI (11) 13 NIL)
;AB2(Z)⊃AB(Z)
;deps: (4)

15. (DERIVE |∀Z.AB2(Z)⊃AB(Z)| (14) NIL)
;∀Z.AB2(Z)⊃AB(Z)
;deps: (4)

16. (DERIVE |∀X.¬AB2(ASPECT1(X))⊃¬FLIES2(X)| (5 6) NIL)
;∀X.¬AB2(ASPECT1(X))⊃¬FLIES2(X)

17. (DERIVE |∀X.BIRD(X)⊃AB2(ASPECT1(X))| (5 6) NIL)
;∀X.BIRD(X)⊃AB2(ASPECT1(X))

18. (DERIVE |∀X.BIRD(X)∧¬AB2(ASPECT2(X))⊃FLIES2(X)| (5 6) NIL)
;∀X.BIRD(X)∧¬AB2(ASPECT2(X))⊃FLIES2(X)

19. (DERIVE |∀X.OSTRICH(X)⊃AB2(ASPECT2(X))| (5 6) NIL)
;∀X.OSTRICH(X)⊃AB2(ASPECT2(X))

20. (DERIVE |∀X.OSTRICH(X)⊃¬FLIES2(X)| (5 6) NIL)
;∀X.OSTRICH(X)⊃¬FLIES2(X)

21. (DERIVE |∀X.OSTRICH(X)∧¬AB2(ASPECT3(X))⊃¬FLIES2(X)| (20) NIL)
;∀X.OSTRICH(X)∧¬AB2(ASPECT3(X))⊃¬FLIES2(X)

22. (DERIVE
      |(∀X.¬AB2(ASPECT1(X))⊃¬FLIES2(X))∧(∀X.BIRD(X)⊃AB2(ASPECT1(X)))∧
       (∀X.BIRD(X)∧¬AB2(ASPECT2(X))⊃FLIES2(X))∧(∀X.OSTRICH(X)⊃AB2(ASPECT2(X)))∧
       (∀X.OSTRICH(X)∧¬AB2(ASPECT3(X))⊃¬FLIES2(X))|
 (16 17 18 19 20 21) )
;(∀X.¬AB2(ASPECT1(X))⊃¬FLIES2(X))∧(∀X.BIRD(X)⊃AB2(ASPECT1(X)))∧
;(∀X.BIRD(X)∧¬AB2(ASPECT2(X))⊃FLIES2(X))∧(∀X.OSTRICH(X)⊃AB2(ASPECT2(X)))∧
;(∀X.OSTRICH(X)∧¬AB2(ASPECT3(X))⊃¬FLIES2(X))

23. (UE ((AB.|AB2|) (FLIES.|FLIES2|)) 1 NIL)
;A(AB2,FLIES2)≡
;(∀X.¬AB2(ASPECT1(X))⊃¬FLIES2(X))∧(∀X.BIRD(X)⊃AB2(ASPECT1(X)))∧
;(∀X.BIRD(X)∧¬AB2(ASPECT2(X))⊃FLIES2(X))∧(∀X.OSTRICH(X)⊃AB2(ASPECT2(X)))∧
;(∀X.OSTRICH(X)∧¬AB2(ASPECT3(X))⊃¬FLIES2(X))

24. (RW 23 (USE 22))
;A(AB2,FLIES2)

25. (DERIVE |∀Z.AB(Z)≡AB2(Z)| (9 15 24) NIL)
;∀Z.AB(Z)≡AB2(Z)
;deps: (4)

;***   failed to derive 
;***   ∀Z.AB(Z)≡AB2(Z)

26. (RW 8 (USE 1 MODE: EXACT))
;(∀X.¬AB(ASPECT1(X))⊃¬FLIES(X))∧(∀X.BIRD(X)⊃AB(ASPECT1(X)))∧
;(∀X.BIRD(X)∧¬AB(ASPECT2(X))⊃FLIES(X))∧(∀X.OSTRICH(X)⊃AB(ASPECT2(X)))∧
;(∀X.OSTRICH(X)∧¬AB(ASPECT3(X))⊃¬FLIES(X))
;deps: (4)

27. (RW 26 ((USE 25 MODE: EXACT) (OPEN AB2)))
;(∀X.¬(∃X1.BIRD(X1)∧X=X1)⊃¬FLIES(X))∧
;(∀X.BIRD(X)∧¬(∃X2.OSTRICH(X2)∧X=X2)⊃FLIES(X))∧(∀X.OSTRICH(X)⊃¬FLIES(X))
;deps: (4)

28. (DERIVE |∀X.FLIES(X)≡BIRD(X)∧¬OSTRICH(X)| (27) NIL)
;∀X.FLIES(X)≡BIRD(X)∧¬OSTRICH(X)
;deps: (4)